Inference at * 1 1 2 
Iof proof for Lemma add functionality wrt le:



1. i2 : 
2. j2 : 
3. i2  j2
4. j1 : 
5. 0  j1
  (0+i2)  (j1+j2) 

latex

 by (RA (IntInd 4)) 

latex

 1: 

 1: 5. 0 < j1
 1: 6. (0  (j1 - 1))  ((0+i2)  ((j1 - 1)+j2))
 1: 7. 0  j1
 1:   (0+i2)  (j1+j2)
 .

Definitions	t  T, False, A, P  Q, A  B, x:A. B(x),
Lemmas	le wf